#ifndef MODEL_H
#define MODEL_H
#include "core/Solver.h"
#include <vector>
#include <string>
#include "valuation.h"
extern "C"
{
	#include "core/aiger.h"
}

namespace cdnf{

class Model{
public:		
	Model(std::string name);
	void loadCNF(std::string filename,Minisat::Solver& solver);
	void loadInitSolver(Minisat::Solver& solver);
	void loadTransitionSolver(Minisat::Solver& solver);
	void loadPropertySolver(Minisat::Solver& solver);
	void loadPropertySolver(Minisat::Solver& solver, bool offset);
	void loadMap();	
	//std::vector<int> simulate(bool* pre,bool* post,bool* input);
	std::vector<int> simulate(Valuation pre,std::vector<int> post,bool* input);
	void aig2cnf();
	~Model();
	int numberOfVar;
	int latch;
	int input;
	int output;
	int nextOutput;
	int maxIndex;
	int offset;
	int* vars;
	bool flag;	
private:
	std::string name;
	aiger* netlist;
	int* nextVars;
	std::vector<std::string> split(const std::string& src);
	int nextVar(int current);
};

}
#endif
